the_w:World, i:Id, a:Action(i). ((isnull(a)))  (kind(a)  Knd) 

latex

Definitions	x:A. B(x), Action(i), P  Q, isnull(a), t  T, kind(a), w.TA, w.M, t.1, t.2, outr(x), True, x. t(x), isl(x), World, Action(dec), A, b, tt, ff, if b then t else f fi , False, x(s),
Lemmas	not wf, assert wf, action wf, w-action-dec wf, Id wf, world wf, pi1 wf, Knd wf, btrue wf, bfalse wf